import datetime
from django.db import models
from django.utils.translation import ugettext_lazy as _

class Todo(models.Model):
    """
    
    inv::
    
        self.status in [s[0] for s in self.STATUS_CHOICES]
        
        ( not (self.deadline and self.created)
            or self.deadline > self.created)
        
    """
    
    STATUS_TODO = "todo"
    STATUS_DOING = "doing"
    STATUS_DONE = "done"
    
    STATUS_CHOICES = (
        (STATUS_TODO, _("Todo")),
        (STATUS_DOING, _("Doing")),
        (STATUS_DONE, _("Done")),
    )
    
    MAX_MULTITASKING = 3
    
    todo = models.TextField()
    
    created = models.DateTimeField(editable=False)
    done = models.DateTimeField(null=True, blank=True, editable=False)
    deadline = models.DateTimeField(null=True, blank=True)
    
    status = models.CharField(max_length=10, choices=STATUS_CHOICES, default=STATUS_TODO)
    
    def __unicode__(self):
        return self.todo[:10]
    
    def save(self):
        """
        pre::
            
            implies(self.status == self.STATUS_DOING,
                Todo.objects.filter(status__exact=self.STATUS_DOING).count() < self.MAX_MULTITASKING)
                
        post[self.id, self.done]::
            
            implies(self.status == self.STATUS_DONE and not __old__.self.done, self.done)
            
            implies(not __old__.self.id,
                self.created and self.created <= datetime.datetime.now())
            
        """
        
        if self.status == self.STATUS_DONE and not self.done:
            self.done = datetime.datetime.now()
        
        if not self.id:
            self.created = datetime.datetime.now()
        
        super(Todo, self).save()

